\documentclass[a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[brazil]{babel}
\usepackage{listings}
\usepackage{indentfirst}
\renewcommand{\familydefault}{\sfdefault}
\renewcommand{\lstlistingname}{Listagem}
\usepackage[margin=2.5cm,noheadfoot]{geometry}
\usepackage{graphicx}
\usepackage{caption}
\begin{document}

\lstset{%language=Pascal,
basicstyle=\footnotesize,       % the size of the fonts that are used for the code
numbers=left,                   % where to put the line-numbers
numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
%showspaces=false,               % show spaces adding particular underscores
%showstringspaces=false,         % underline spaces within strings
%showtabs=false,                 % show tabs within strings adding particular underscores
frame=single,	                % adds a frame around the code
tabsize=2,	                % sets default tabsize to 2 spaces
%captionpos=b,                   % sets the caption-position to bottom
%breaklines=true,                % sets automatic line breaking
%breakatwhitespace=false,        % sets if automatic breaks should only happen at whitespace
%title=\lstname,                 % show the filename of files included with \lstinputlisting; also try caption instead of title
%escapeinside={\%*}{*)}          % if you want to add a comment within your code
}

\include{capa}

\tableofcontents
\newpage

\section{Introdução}

O presente trabalho propõe a verificação automática de modelos utilizando-se a ferramenta NuSMV. Os modelos escolhidos para verificação foram os de um registrador de deslocamento e de um multiplexador. São ambos modelos simples, mas que servem de aprendizado na utilização da ferramenta e de sua linguagem de entrada.

Além desses modelos, pensou-se em um terceiro, que modela o funcionamento de um elevador. Entretanto, as dificuldades de implementação encontradas foram maiores que o esperado e, por isso, decidiu-se fazer desse modelo um estudo de caso para esse trabalho. Sua implementação pode ser o tema de trabalhos futuros.


\section{Objetivos}

Os principais objetivos do trabalho são:

\begin{itemize}
 \item Familiarizar-se com a ferramenta de verificação de modelos \textit{NuSMV};
 \item Aprender um pouco da linguagem para verificação de modelos utilizada por essa ferramenta;
 \item Especificar propriedades lógicas consistentes para validação de modelos síncronos/assíncronos através de: \textit{CTL Model Checking}, \textit{LTL Model Checking} e \textit{Bounded Model Checking}.
\end{itemize}

\section{Modelos}

Para desenvolver os conceitos que envolvem os \textit{Symbolic Model Checkers}, foram propostos dois problemas bem simples a serem modelados, assim como definidas algumas propriedades a serem provadas para cada um deles. Os modelos propostos são de um registrador de deslocamento e de um multiplexador.

  \subsection{Registrador de Deslocamento}

\lstinputlisting[caption=Modelo do Registrador de Deslocamento]{../src/register.smv}

Um registrador de deslocamento é composto por um conjunto de \textit{flip-flops} ligados em série, em que a saída de um deles serve de entrada para o próximo e assim por diante. São usados para transferência de dados em projeto de computadores, já que eles apenas transferem o dado de entrada recebido em um período de tempo para a sua saída no próximo intervalo de tempo. Um exemplo mais comum pode ser encontrado em letreiros luminosos, nos quais as letras são movimentadas através de tipos semelhantes a estes registradores.

As propriedades a serem provadas são simples, mas definem o comportamento do dispositivo.\\

\verb"LTLSPEC F ( reg2.out = reg1.out)"

É verdade que em algum futuro as saídas dos registradores reg2 e reg1 serão iguais. Se uma sequencia de valores iguais forem atribuídos na entrada do registrador reg0, isso é possível.\\

\verb"LTLSPEC G ( reg0.out = 3 -> X reg1.out = 3 )"

É globalmente verdadeiro que se na saída de um registrador $n$ temos um valor $v$, no próximo estado a saída do registrador $n+1$ terá esse valor $v$. Essa é a propriedade básica dos registradores de deslocamento.\\

\verb"LTLSPEC G ( reg0.out = 3 -> X reg2.out = 3 )"

É globalmente verdadeiro que se na saída de um registrador $n$ temos um valor $v$, no próximo estado a saída do registrador $n+2$ terá esse valor $v$. Isso é falso, devido ao que foi explicado anteriormente para os registradores de deslocamento.\\

\verb"LTLSPEC G F ( reg0.out = 1 | reg0.out = 2 | reg0.out = 3)"

É globalmente verdadeiro que em um futuro as saídas de todos os registradores terão um desses valores {1, 2, 3}.\\

\verb"LTLSPEC ! G F ( reg0.out = 4 )"

Não é globalmente verdadeiro que a saída de algum registrador terá o valor 4. Na modelagem os valores de saídas foram limitados de 1 a 3.
  \subsection{Multiplexador 4 X 1}

Em circuitos digitais, o multiplexador tem a capacidade de receber fluxos de dados distintos em suas entradas e combiná-los num único fluxo de dados com uma taxa de transferência  alta. A sua arquitetura também é bem simples: no caso em questão temos um multiplexador de 4 entradas e uma chave seletora. Para cada valor da chave seletora, uma das entradas é chaveada para a saída. Isto permite que múltiplos fluxos de dados sejam transportados de um local para outro através de uma única ligação física, sendo que apenas uma entrada é selecionada de cada vez.

\begin{center}
	\includegraphics[scale=1.00]{fig.png}
	\captionof{figure}{Multiplexador Digital}
	\label{fig:mux}
\end{center}

A modelagem em \textit{SMV} é mostrada abaixo:
  
\lstinputlisting[caption=Modelo do Multiplexador]{../src/mux.smv}

Propriedades provadas:\\

\verb"LTLSPEC G F( select = 3 & in3 = 1 -> X m1.out = 1 )"\\

\verb"LTLSPEC G F( select = 0 & in0 = 2 -> X m1.out = 2 )"\\

É globalmente verdade que se a chave seletora for $x$ e a entrada $x$ tiver um valor $v$, esse valor será selecionado para a saída no próximo estado.\\

\verb"LTLSPEC G F( select = 1 & in0 = 3 -> X m1.out = 3 )"

Essa especificação é falsa. Nota-se que ela é uma contradição em relação as duas anteriormente citadas, não há uma relação entre a chave seletora com um valor $x$ e uma entrada diferente de $x$ ser selecionada para a saída.

\section{Resultados das Verificações}

\subsection{Registrador de Deslocamento}

\begin{lstlisting}[caption=Saída]
-- specification  F reg2.out = reg1.out  is true
-- specification  G (reg0.out = 3 ->  X reg1.out = 3)  is true
-- specification  G (reg0.out = 3 ->  X reg2.out = 3)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  data = 3
  reg0.value = 0
  reg1.value = 0
  reg2.value = 0
  reg0.out = 0
  reg1.out = 0
  reg2.out = 0
-> Input: 1.2 <-
-> State: 1.2 <-
  reg0.value = 3
  reg0.out = 3
-> Input: 1.3 <-
-> State: 1.3 <-
  reg1.value = 3
  reg1.out = 3
-> Input: 1.4 <-
-- Loop starts here
-> State: 1.4 <-
  reg2.value = 3
  reg2.out = 3
-> Input: 1.5 <-
-> State: 1.5 <-
-- specification  G ( F ((reg0.out = 1 | reg0.out = 2) | reg0.out = 3))  is true
-- specification !( G ( F reg0.out = 4))  is true
\end{lstlisting}

\subsection{Multiplexador 4 X 1}
\begin{lstlisting}[caption=Saída]
-- specification  G ((select = 0 & in0 = 2) ->  X m1.out = 2)  is true
-- specification  G ((select = 1 & in0 = 3) ->  X m1.out = 3)  is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample 
-> State: 1.1 <-
  in0 = 2
  in1 = 2
  in2 = 2
  in3 = 2
  select = 0
  m1.value = 0
  m1.out = 0
-> Input: 1.2 <-
-> State: 1.2 <-
  in0 = 3
  in2 = 1
  in3 = 1
  select = 1
  m1.value = 2
  m1.out = 2
-> Input: 1.3 <-
-- Loop starts here
-> State: 1.3 <-
  in0 = 2
  in2 = 2
  in3 = 2
  select = 0
-> Input: 1.4 <-
-> State: 1.4 <-
-- specification  G ((select = 3 & in3 = 1) ->  X m1.out = 1)  is true
\end{lstlisting}
\section{Estudo de Caso: Modelagem de um Elevador}

A primeira proposta de modelagem que tivemos em mente foi a de um elevador. Um elevador pode ser descrito através de estados e transições, que são realizadas através de um evento externo. É possível definir uma máquina de estados finitos para um elevador de tal forma que modelo atenda às necessidades de um determinado ambiente, pois sabemos que elevadores são projetados com comportamentos distintos de acordo com sua utilização.

Um elevador inicia seu funcionamento em um estado inicial que corresponde ao andar que ele está parado. Várias ações são possíveis ao longo de seu funcionamento:

\begin{enumerate}
  \item Porta aberta: elevador não se move;
  \item Começa a subir ou começa a descer: fecha a porta antes de mudar de estado;
	\item Elevador parado: através de um requisição para subir ele sobe, com uma para descer ele desce;
	\item Elevador subindo: com uma requisição para subir ele continua nesse estado até que todas as requisições nessa direção sejam atendidas;
	\item Elevador descendo: com uma requisição para descer ele continua nesse estado até que todas as requisições nessa direção sejam atendidas;
	\item Elevador subindo: com uma requisição para descer ele armazena aquele pedido, e assim que todas as requisições nessa direção forem atendidas, ele muda de estado e inicia o processo de atendimento àquela solicitação;
	\item Elevador descendo: com uma requisição para subir ele armazena aquele pedido, e assim que todas as requisições nessa direção forem atendidas, ele muda de estado e inicia o processo de atendimento àquela solicitação;
	\item Requisições a atender: se foi feita uma chamada a partir de um andar em uma determinada direção e o andar atual do elevador é igual, assim como direção de atendimento das requisições, o elevador para, abre a porta (pessoa entra), fecha a porta. Ele pode continuar no estado anterior ou mudar de estado com relação à requisição de ir a um determinado andar, feita  pela pessoa que acabou de entrar no elevador.
\end{enumerate}

Foi feita uma tentativa de modelagem desse problema. Mas tivemos bastante dificuldade em entender como o \textit{NuSMV} trata os parâmetros de entrada. De primeiro momento, não entendemos muito bem como gerar as entradas que iríamos precisar nos módulos criados. Outro aspecto é que foi complicado a parte de lógica temporal, em que propriedades são definidas através de estados consecutivos no tempo, sendo que isso é o ponto chave da operação de um elevador.

Como pode ser visto, a descrição do elevador contém uma série de detalhes a serem implementados, fazendo com que sua modelagem e respectiva verificação seja de grande interesse, afim de evitar anomalias de comportamento do mesmo.

Pensamos na possibilidade de abordar este estudo de caso na elaboração do \textit{Trabalho Prático 2}. Através de uma análise mais apurada, notou-se que é um projeto relativamente complexo e que fornece grande possibilidade de aplicar os conceitos de verificação automática vistos em sala de aula.

\section{Conclusões}

Os modelos propostos no trabalho, apesar de simples, foram úteis em um primeiro contato prático com a ferramenta em questão e com a linguagem de entrada utilizada por ela, a qual utiliza os principais conceitos vistos em sala de aula. A implementação desses modelos serviu ainda para expor os autores do trabalho a alguns dos problemas mais comuns nesse tipo de modelagem, como descrito anteriormente.

Conclui-se, então, que o presente trabalho serviu ao seu propósito de fornecer um primeiro contato dos autores com a modelagem de problemas para serem verificados pela ferramenta e linguagem em questão. Serve, ainda, como uma proposta de tema para trabalhos futuros, em uma possível implementação do estudo de caso descrito.

%\newpage
%\appendix
%\section{Listagem dos Códigos Utilizados} \label{apendice}

\lstset{%language=Java,
basicstyle=\footnotesize,       % the size of the fonts that are used for the code
numbers=left,                   % where to put the line-numbers
numberstyle=\footnotesize,      % the size of the fonts that are used for the line-numbers
stepnumber=1,                   % the step between two line-numbers. If it's 1 each line will be numbered
%numbersep=5pt,                  % how far the line-numbers are from the code
%backgroundcolor=\color{white},  % choose the background color. You must add \usepackage{color}
%showspaces=false,               % show spaces adding particular underscores
showstringspaces=false,         % underline spaces within strings
%showtabs=false,                 % show tabs within strings adding particular underscores
frame=single,	                % adds a frame around the code
tabsize=2,	                % sets default tabsize to 2 spaces
%captionpos=b,                   % sets the caption-position to bottom
%breaklines=true,                % sets automatic line breaking
%breakatwhitespace=false,        % sets if automatic breaks should only happen at whitespace
%title=\lstname,                 % show the filename of files included with \lstinputlisting; also try caption instead of title
%escapeinside={\%*}{*)}          % if you want to add a comment within your code
extendedchars=true,
inputencoding=utf8
}

%\subsection{Listagem dos Códigos-Fontes}
%\lstinputlisting[caption=Modelo do Registrador]{../src/register.smv}
%\lstinputlisting[caption=Modelo do Multiplexador]{../src/mux.smv}

%\nocite{*}
%\bibliographystyle{plain}
%\bibliographystyle{apalike}
%\renewcommand{\refname}{Referências}
%\addcontentsline{toc}{section}{Referências}
%\bibliography{referencias}

\end{document}
